x:chain_master(). (cmseq?(x))  (cmseq-to(x)  Id) 

latex

Definitions	s = t, t  T, True, Id, , x:AB(x), P  Q, False, type List, chain master ind cmseq compseq tag def, b, cmseq?(x), chain master ind cmconfig compseq tag def, x:A  B(x), left + right, chain_master(), cmseq-to(x), x:A. B(x)
Lemmas	assert wf, cmseq? wf, chain master wf, false wf, true wf